open util/integer

sig string {}

abstract sig Elemento_base {
	data: one Int
}

sig Hotel extends Elemento_base {
}

sig Volo extends Elemento_base {
}

sig Escursione extends Elemento_base {
}

sig Pacchetto{
	ID: one Int,
	el: set Elemento_base,
	dataAnd: one Int,
	dataRit: one Int
} {dataRit>=dataAnd}

sig Wishlist {
	pack: set Pacchetto
}

sig Carrello {
	pack: set Pacchetto
}

sig Utente_registrato {
	wish: one Wishlist,
	carr: one Carrello,
	username: one string,
	password: one string
}

//Non esistono 2 Pacchetti con lo stesso ID

fact {
	no disj p1,p2: Pacchetto | p1.ID=p2.ID
}

assert IDpsing {
	no i:Int ,disj p1,p2: Pacchetto | p1.ID=i && p2.ID=i
}

//check IDpsing for 5

//Non esistono 2 Utenti_registrati con lo stesso username (ma possono avere la stessa password)

fact {
	no disj u1,u2: Utente_registrato | u1.username=u2.username
}

assert usersing {
	no s:string ,disj u1,u2: Utente_registrato | u1.username=s && u2.username=s
}

//check usersing for 5

//Non esistono string che non siano associate a un utente

fact {
	all s:string | some u:Utente_registrato | s in u.username or s in u.password
}

assert nos {
	not (some s:string| no u:Utente_registrato | s in u.username or s in u.password)
}

//check nos for 5

//Non esistono Carrelli o Wishlist che non siano associati a un utente

fact {
	all c:Carrello | some u:Utente_registrato | c in u.carr
}

fact {
	all w:Wishlist | some u:Utente_registrato | w in u.wish
}

assert noc {
	not (some c:Carrello| no u:Utente_registrato | c in u.carr)
}

assert now {
	not (some w:Wishlist| no u:Utente_registrato | w in u.wish)
}

//check noc for 5
//check now for 5

// Non esistono 2 utenti che hanno lo stesso carrello

fact {
	no disj u1,u2: Utente_registrato | u1.carr=u2.carr
}

assert carrsing {
	no c:Carrello ,disj u1,u2: Utente_registrato | u1.carr=c && u2.carr=c
}

//check carrsing for 5

// Non esistono 2 utenti che hanno la stessa wishlist

fact {
	no disj u1,u2: Utente_registrato | u1.wish=u2.wish
}

assert wishsing {
	no w:Wishlist ,disj u1,u2: Utente_registrato | u1.wish=w && u2.wish=w
}

//check wishsing for 5

// Tutti gli elementi del viaggio sono compresi fra data di andata e quella di ritorno

fact {
	no p:Pacchetto,e: Elemento_base | e in p.el && (e.data > p.dataRit or e.data < p.dataAnd)
}

assert dateok {
	all p:Pacchetto,e:Elemento_base | (e in p.el) implies (e.data <= p.dataRit and e.data >= p.dataAnd)
}

//check dateok

// Tutti i pacchetti iniziano e finiscono con un volo

fact {
	all p:Pacchetto| some disj v1,v2:Volo | v1 in p.el && v2 in p.el && v1.data=p.dataAnd && v2.data=p.dataRit
}

assert noflight {
	no p:Pacchetto | all v:Volo | v in p.el && !(v.data=p.dataAnd or v.data=p.dataRit)
}

//check noflight

// Crea mondo

pred show () {}

run show for 5
